LTL to Deterministic Emerson-Lei Automata

摘要

We introduce a new translation from linear temporal logic (LTL) todeterministic Emerson-Lei automata, which are omega-automata with a Mulleracceptance condition symbolically expressed as a Boolean formula. The richeracceptance condition structure allows the shift of complexity from the statespace to the acceptance condition. Conceptually the construction is an enhancedproduct construction that exploits knowledge of its components to reduce thenumber of states. We identify two fragments of LTL, for which one can easilyconstruct deterministic automata and show how knowledge of these components canreduce the number of states. We extend this idea to a general LTL framework,where we can use arbitrary LTL to deterministic automata translators for partsof formulas outside the mentioned fragments. Further, we show succinctness ofthe translation compared to existing construction. The construction isimplemented in the tool Delag, which we evaluate on several benchmarks of LTLformulas and probabilistic model checking case studies.